On Practical SMT-Based Type Error Localization

摘要

Compilers for statically typed functional programming languages are notoriousfor generating confusing type error messages. When the compiler detects a typeerror, it typically reports the program location where the type checking failedas the source of the error. Since other error sources are not even considered,the actual root cause is often missed. A more adequate approach is to considerall possible error sources and report the most useful one subject to someusefulness criterion. In our previous work, we showed that this approach can beformulated as an optimization problem related to satisfiability modulo theories(SMT). This formulation cleanly separates the heuristic nature of usefulnesscriteria from the underlying search problem. Unfortunately, algorithms thatsearch for an optimal error source cannot directly use principal types whichare crucial for dealing with the exponential-time complexity of the decisionproblem of polymorphic type checking. In this paper, we present a new algorithmthat efficiently finds an optimal error source in a given ill-typed program.Our algorithm uses an improved SMT encoding to cope with the high complexity ofpolymorphic typing by iteratively expanding the typing constraints from whichprincipal types are derived. The algorithm preserves the clean separationbetween the heuristics and the actual search. We have implemented our algorithmfor OCaml. In our experimental evaluation, we found that the algorithm reducesthe running times for optimal type error localization from minutes to secondsand scales better than previous localization algorithms.